es:ES, i, a:Id, T:Type, ds:x:Id fp Type, P:(State(ds)TProp).
@i Precondition for a(v)P State(ds) (v:T)  Prop 

latex

Definitions

@i state ds, x:A. B(x), t  T, P  Q, state@i, State(ds), es_init(es), f(a), loc(e), Id, s = t, E, x:AB(x), x:A. B(x), P & Q, Type, Prop, x:AB(x), b, Void, False, A, ES, Atom$n, a:A fp B(a), locl(a), A/x,y. B(x;y), 1of(t), left+right, P  Q, e  e' , Top, IdDeq, x.A(x), x. t(x), f(x)?z, vartype(i;x), state after e, kind(e), Knd, A & B, val(e), (state when e), valtype(e), e@i. P(e), ee'.P(e'), @i Precondition for a(v)P State(ds) (v:T)

Lemmas

decl-state wf, fpf wf, event system wf, es-valtype wf, es-state-when wf, es-val wf, es-le wf, Knd wf, es-kind wf, locl wf, not wf, es-state-after wf, subtype rel dep function, subtype rel self, es-vartype wf, fpf-cap wf, id-deq wf, top wf, es-le-loc, es-loc-pred, es-E wf, Id wf, es-loc wf, es init wf, es-state-type-implies